(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, comp_f_g#1(x1, x2, 0))
comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0)
map#2(Nil) → Nil
map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6))
plus_x#1(0, x6) → x6
plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10))
foldr_f#3(Nil, 0) → 0
foldr_f#3(Cons(x16, x5), x24) → comp_f_g#1(x16, foldr#3(x5), x24)
foldr#3(Nil) → id
foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6))
main(x3) → foldr_f#3(map#2(x3), 0)
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6]
transitions:
plus_x0(0) → 0
comp_f_g0(0, 0) → 0
00() → 0
id0() → 0
Nil0() → 0
Cons0(0, 0) → 0
S0(0) → 0
comp_f_g#10(0, 0, 0) → 1
map#20(0) → 2
plus_x#10(0, 0) → 3
foldr_f#30(0, 0) → 4
foldr#30(0) → 5
main0(0) → 6
01() → 8
comp_f_g#11(0, 0, 8) → 7
plus_x#11(0, 7) → 1
01() → 9
plus_x#11(0, 9) → 1
Nil1() → 2
plus_x1(0) → 10
map#21(0) → 11
Cons1(10, 11) → 2
plus_x#11(0, 0) → 12
S1(12) → 3
01() → 4
foldr#31(0) → 13
comp_f_g#11(0, 13, 0) → 4
id1() → 5
foldr#31(0) → 14
comp_f_g1(0, 14) → 5
map#21(0) → 15
01() → 16
foldr_f#31(15, 16) → 6
plus_x#11(0, 7) → 7
plus_x#11(0, 9) → 7
Nil1() → 11
Nil1() → 15
Cons1(10, 11) → 11
Cons1(10, 11) → 15
plus_x#11(0, 7) → 12
S1(12) → 1
plus_x#11(0, 9) → 12
S1(12) → 12
id1() → 13
id1() → 14
comp_f_g1(0, 14) → 13
comp_f_g1(0, 14) → 14
comp_f_g#11(0, 14, 8) → 7
plus_x#11(0, 7) → 4
plus_x#11(0, 9) → 4
S1(12) → 7
02() → 6
foldr#32(11) → 17
comp_f_g#12(10, 17, 16) → 6
id2() → 17
foldr#32(11) → 18
comp_f_g2(10, 18) → 17
id2() → 18
comp_f_g2(10, 18) → 18
02() → 20
comp_f_g#12(10, 18, 20) → 19
plus_x#12(0, 19) → 6
02() → 21
plus_x#12(0, 21) → 6
plus_x#12(0, 19) → 19
plus_x#12(0, 21) → 19
plus_x#11(0, 19) → 12
S1(12) → 6
plus_x#11(0, 21) → 12
S1(12) → 19
0 → 3
0 → 12
7 → 1
7 → 12
7 → 4
9 → 1
9 → 7
19 → 6
19 → 12
21 → 6
21 → 12
21 → 19
(2) BOUNDS(1, n^1)